Encoding Equilibrium (DNM) by balacij · Pull Request #4058 · JacquesCarette/Drasil

balacij · 2025-05-09T20:18:34Z

Do Not Merge (DNM).

We can use this to discuss encoding equilibrium in Drasil and spin issues off this PR if necessary.

I will annotate the PR first.

I've only encoded equilibrium in the context of a simple supply/demand curve thus far.

balacij

The bulk of the comments.

balacij · 2025-05-09T20:27:35Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

-        , TMs [] []
+        , TMs [] (Label : stdFields)
        , GDs [] [] HideDerivation
-        , DDs [] [] HideDerivation
-        , IMs [] [] HideDerivation
+        , DDs [] (Label : stdFields) HideDerivation
+        , IMs [] ([Label, Input, Output, InConstraints, OutConstraints] ++ stdFields) HideDerivation


Input, Output, (In/Out)Constraints are rows that are only permitted for IMs. I'm not quite sure why. Are "inputs" not the input variables of a hypothetical function being defined?

That's because 'definitions' don't have input/output, and many theories are relational, so again input/output makes no sense for them.

I'm not quite sure I'm following. What is the difference between a data definition (which defines QDefinitions) and an EquationalModel-based (i.e., QDefinition-defining) instance model?

Is "input/output" in regard to the "system's" inputs, outputs, and intermediate variables? If so, I think that should still be relevant to data definitions, which can be used to interpret input variables to intermediate variables (e.g., for unit conversion, etc.), no?

Do remember that "F = ma" is usually used to get 'a' as output, given F and m as input!

I think we ought to use different vocabulary for input and output of a system, and equations where some variables can be substituted for.

It is true that the intent of a data definition is that the new symbol is defined by the computation where we imagine substituting for the (implicitly occuring) variables in the RHS. A data-definition is implicitly a function.

balacij · 2025-05-09T20:30:20Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

-  _quants      = [] :: [QuantityDict],
-  _instModels  = [] :: [InstanceModel],
-  _datadefs    = [] :: [DataDefinition],
+  _quants      = quantities, -- Odd: The Table of Symbols is mostly filled without this list!!!! Also, even though the table of symbols is being filled in, there is text "There are no symbols." placed above the table!
+  _instModels  = instanceModels, -- Surprisingly, putting this here is not what triggers it to get rendered.
+  _datadefs    = dataDefinitions, -- ^


This is something that needs to be spun off into 2 new tickets.

The SRS is rendered using the instance models and data definitions taken from the ChunkDB rather than here. We should probably change that.

The Table of Symbols is partially rendered without filling in the _quants field, but completely filled in when passing this list to it. This should be investigated a little bit more.

The deeper questions are:

where should the information come from? We used to do things "by hand" because there was no other choice. But, of course, Drasil should automate things as much as possible. So it is a good thing that some information comes from the theories rather than hand-built!

what is the difference between the "background information" necessary, and the meta-data needed to build a particular system? And should that information be gathered? Divided up?

balacij · 2025-05-09T20:30:49Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibrium :: IdeaDict
+equilibrium = nc "equilibrium" $ nounPhrase "equilibrium" "equilibria"


Once defined, never used! Should we be using it? If so, how?

Never used because you're not "doing it right". For example, it should have been used on line 295, and indeed on line 202 as well.

Unfortunately, none of the constructors for QuantityDicts let us give them a plain IdeaDict. All of the constructors are keen on extracting an IdeaDict from something else or creating one that is immediately associated with the Q-D-.

I don't understand. On line 295, you could have gotten the nounPhrase by using the lens defined for that. What do you think the code should instead look like?

I would have expected to be able to pass in the entire IdeaDict (seeing as QuantityDicts currently nest an IdeaDict), and for the QuantityDict to only carry a UID reference to said IdeaDict.

You have the power to change Drasil: do it! Introduce new functions that let you do that. That's the fun part, of seeing things that should be better, and just improving them.

balacij · 2025-05-09T23:29:25Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibriumQ :: QuantityDict
+equilibriumQ = mkQuant' -- A somewhat odd variant of `mkQuant` that re-orders argument and adds staging to the `Symbol`
+  "inEquilibrium"
+  (nounPhrase "in equilibrium" "all equilibria") -- duplicates the IdeaDict
+  Nothing -- UnitDefn
+  Boolean
+  (autoStage $ label "inEquilibrium")
+  Nothing -- "abbreviation String"


QuantityDict's mkQuant' and related smart constructors are interesting because they create their own IdeaDicts that they associate with themselves. QDefinition's mkQuantDef and related smart constructors are similar, except they also create a DefinedQuantityDict, which also creates a ConceptChunk. In the future, it might be that our smart constructors are stateful too (in reference to #2873 (comment)).

This is indeed a sign that we're trying to be too clever. We need to rethink this.

balacij · 2025-05-09T23:30:41Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+priceQ = mkQuant'
+  "priceQuant" -- duplicates the IdeaDict
+  (cn "price")
+  Nothing -- UnitDefn // FIXME: Uh oh! There's seemingly no way we can define a new unit: $CAD.s


I was expecting that I wouldn't be able to create numbers of the form $ X CAD, but that I would be able to create CAD units at least. I don't see a clear way to doing that without it being 'derived' from the SI unit system.

I'm not sure that currencies are 'units', per se. They are a classification system, and we ought to support more of them than just SI.

Ah, I hadn't realized that UnitDefn and our unit system in general was only meant for physical quantities following the SI.

Right - it's a side-effect of Drasil being focused on scientific software, so that was the most important classification system. Types were second. Now we might need more classification systems to be added (and most likely, our code refactored to reflect this fact.)

balacij · 2025-05-10T22:37:45Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+-- ^ I'm deliberately choosing to use applePrice here because I want to use this
+-- in an instance model, which (I believe) should mean that there are only
+-- 'concrete' variables (i.e., problem-related variables, not the abstract ones
+-- imported from the hypothetical library that would contain equilibrium)


How can/should we differentiate between abstract and concrete variables?

We should. Don't know if we currently can.

balacij · 2025-05-10T23:07:25Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+  (cn "equilibrium apple price")
+  Nothing -- UnitDefn
+  Real -- Space
+  (autoStage $ sub lP $ label "A,Eq") -- Hack because of lack of support for symbol "corners" in Drasil.


lack of adequate support*. Related to #1606.

balacij · 2025-05-11T05:51:27Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibriumPriceLinearSDQIM :: InstanceModel
+equilibriumPriceLinearSDQIM = imNoDerivNoRefs
+  (equationalModel' equilibriumApplePriceLinearSDQD)
+  [] -- Inputs -- What are they? Why is this only here and not in the TM?
+  equilibriumApplePriceLinearSDQ -- Output -- not everything will have an output!
+  [UpFrom (Exc, int 0)] -- Output constraints: price > 0 -- why can't I put gtZerConstr
+  "equilibriumApplePriceIM"
+  [] -- Notes ([Sentence])


The important bit is really the QDefinition, which contains a DefinedQuantityDict (DQD) and a defining formula for the DQD. Now:

What are the "inputs"? If the DQD is a function (i.e., a function-typed variable), is it the inputs to the function? In Projectile's IM:calOfLandingDist, $p_\text{land}$ is noted as having two inputs: $v_\text{launch}$ and $\theta$, but $p_\text{land}$ is not a function. If it should be (and I don't think it should be), then why is $g$ not a part of its inputs?

Why isn't the list of input and output variables and their corresponding constraints in the QDefinition. Same with the notes. Why wouldn't they be part of the QDefinition?

While we're here, why not the derivation and the references?

I think input and output are / ought to be theory-level concepts and not chunk-level.

I agree that input and output should be at the theory level.

For the specific example of $p_\text{land}$, $g$ is not an input because it is a constant. Having $g$ as a constant is a modelling choice (assumption). If we were at a different elevation, or on a different planet, $g$ would be different. Drasil shouldn't force us to have one model for any part of physics (or any other science). With different assumptions, we get different models. In the projectile SRS we have gravAccelValue (The acceleration due to gravity is assumed to have the value provided in the section for Values of Auxiliary Constants). If this assumption is removed, we would have $g$ as an input (runtime variability for $g$). We could also have a different binding time for $g$ if we supported program families. We could set the binding time for $g$ as the specification time. We almost have this now, but it would have to be changed manually, instead of the specification being explicitly parameterized by its variabilities.

balacij · 2025-05-11T05:52:41Z

code/drasil-lang/lib/Language/Drasil/Chunk/Eq.hs

+{-
+  DefinedQuantityDict seems like a wart. It seems like it's only necessary when
+  we want to assert that a quantity has an English interpretation along with a
+  mathematical one (i.e., a variable).
+-}


It seems like D-Q-D really just wants to be smart constructor as I mentioned earlier. There's no reason why a QuantityDict couldn't also have a description.

balacij · 2025-05-11T05:53:00Z

code/drasil-printers/lib/Language/Drasil/HTML/Print.hs

 -- | Renders definition tables (Data, General, Theory, etc.).
 makeDefn :: L.DType -> [(String,[LayoutObj])] -> Doc -> Doc
-makeDefn _ [] _  = error "L.Empty definition"
+makeDefn _ [] _  = error "Definition table has no designated rows to render!"


Probably something that should just be ported over to main.

JacquesCarette · 2025-05-14T18:59:24Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

-        , TMs [] []
+        , TMs [] (Label : stdFields)
        , GDs [] [] HideDerivation
-        , DDs [] [] HideDerivation
-        , IMs [] [] HideDerivation
+        , DDs [] (Label : stdFields) HideDerivation
+        , IMs [] ([Label, Input, Output, InConstraints, OutConstraints] ++ stdFields) HideDerivation


That's because 'definitions' don't have input/output, and many theories are relational, so again input/output makes no sense for them.

JacquesCarette · 2025-05-14T19:31:58Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

-  _quants      = [] :: [QuantityDict],
-  _instModels  = [] :: [InstanceModel],
-  _datadefs    = [] :: [DataDefinition],
+  _quants      = quantities, -- Odd: The Table of Symbols is mostly filled without this list!!!! Also, even though the table of symbols is being filled in, there is text "There are no symbols." placed above the table!
+  _instModels  = instanceModels, -- Surprisingly, putting this here is not what triggers it to get rendered.
+  _datadefs    = dataDefinitions, -- ^


The deeper questions are:

where should the information come from? We used to do things "by hand" because there was no other choice. But, of course, Drasil should automate things as much as possible. So it is a good thing that some information comes from the theories rather than hand-built!

what is the difference between the "background information" necessary, and the meta-data needed to build a particular system? And should that information be gathered? Divided up?

JacquesCarette · 2025-05-14T19:36:21Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibrium :: IdeaDict
+equilibrium = nc "equilibrium" $ nounPhrase "equilibrium" "equilibria"


Never used because you're not "doing it right". For example, it should have been used on line 295, and indeed on line 202 as well.

JacquesCarette · 2025-05-14T19:37:46Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibriumQ :: QuantityDict
+equilibriumQ = mkQuant' -- A somewhat odd variant of `mkQuant` that re-orders argument and adds staging to the `Symbol`
+  "inEquilibrium"
+  (nounPhrase "in equilibrium" "all equilibria") -- duplicates the IdeaDict
+  Nothing -- UnitDefn
+  Boolean
+  (autoStage $ label "inEquilibrium")
+  Nothing -- "abbreviation String"


This is indeed a sign that we're trying to be too clever. We need to rethink this.

JacquesCarette · 2025-05-14T19:40:02Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+
+priceQ :: QuantityDict
+priceQ = mkQuant'
+  "priceQuant" -- duplicates the IdeaDict


It is technically a duplication -- but it shouldn't be, because the 'concept' of a price, and a variable that holds a 'price' value are completely different. And the bug is that you shouldn't do (cn "price") below but refer to price ^. term instead.

JacquesCarette · 2025-05-14T19:48:53Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+  Nothing -- UnitDefn
+  (mkFunction [Real] Integer)
+  (autoStage $ sub cS lL)
+  Nothing -- Abbreviation


SCS has tons of abbreviations. Maybe it's just that finance has less so for fundamental quantities?

JacquesCarette · 2025-05-14T19:51:13Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+linearDemandQ :: QuantityDict
+linearDemandQ = mkQuant'
+  "linearDemandQuant"
+  (pn "price-dependant apple demand")


here all the pns below: I think you're abusing pn here, a different constructor should be used.

Also, these 'noun phrases' should be built compositionally! The word 'apple' should never be repeated or even mentioned in all of thse (in the source). Similarly, demand, marginal, supply and price should all be abstracted.

JacquesCarette · 2025-05-14T19:51:50Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+-- ^ I'm deliberately choosing to use applePrice here because I want to use this
+-- in an instance model, which (I believe) should mean that there are only
+-- 'concrete' variables (i.e., problem-related variables, not the abstract ones
+-- imported from the hypothetical library that would contain equilibrium)


We should. Don't know if we currently can.

JacquesCarette · 2025-05-14T19:52:16Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+linearSupplyDD = ddENoRefs
+  linearSupplyQD
+  Nothing -- Derivation
+  "linearSupplyDD" -- "ShortName"


I thought short names were for human consumption!?

JacquesCarette · 2025-05-14T19:54:06Z

code/drasil-example/template/lib/Drasil/Template/Body.hs

+equilibriumPriceLinearSDQIM :: InstanceModel
+equilibriumPriceLinearSDQIM = imNoDerivNoRefs
+  (equationalModel' equilibriumApplePriceLinearSDQD)
+  [] -- Inputs -- What are they? Why is this only here and not in the TM?
+  equilibriumApplePriceLinearSDQ -- Output -- not everything will have an output!
+  [UpFrom (Exc, int 0)] -- Output constraints: price > 0 -- why can't I put gtZerConstr
+  "equilibriumApplePriceIM"
+  [] -- Notes ([Sentence])


I think input and output are / ought to be theory-level concepts and not chunk-level.

balacij added 5 commits May 9, 2025 13:30

Working on Equilibrium

61d1f6f

Rendering equilibrium in the template

1e598b1

Add DDs

daec46b

Fill in quantities, rename variables

213bf77

Refinements

c30fd28

balacij commented May 11, 2025

View reviewed changes

Merge branch 'main' into equilibrium

ec72914

JacquesCarette reviewed May 14, 2025

View reviewed changes

		equilibrium :: IdeaDict
		equilibrium = nc "equilibrium" $ nounPhrase "equilibrium" "equilibria"

Conversation

balacij commented May 9, 2025

Uh oh!

balacij left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees